COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.<<syntax[w84,jmc]		Syntax and semantics of programs with go to>>
C00010 ENDMK
C⊗;
.<<syntax[w84,jmc]		Syntax and semantics of programs with go to>>
.require "memo.pub[let,jmc]" source;
.cb "Abstract Syntax and Semantics of Programs with %3go to%1"

.cb "by John McCarthy, Stanford University"

.at "qgo" ⊂"%3go_to%*"⊃
.at "qbegin" ⊂"%3begin%*"⊃
.at "qend" ⊂"%3end%*"⊃
.at "qx" ⊂"%Ax%*"⊃
	The object of this note is to give an example of the abstract
syntax and semantics of a programming language (call it ⊗F1)
 which is far from context
free.  We choose programs with assignments, conditionals and qgos,
because we want our syntax to express the fact that for every qgo,
the corresponding label must exist, and no label should occur more
than once.

	The simplest formulation supposes that each assignment statement
has both a label and a qgo.  We identify a statement with the unit
set containing just that statement.  Programs are constructed in
two ways.

.item←0
	#. An elementary statement %2elem(l1,p,f,l2,l3)%1 is a program.
Its intuitive interpretation is

%2l1:∂(10)qif p(qx) qthen qbegin qx ← f(qx); qgo l2 qend qelse qgo l3;%1

Here qx is a state vector, ⊗p is a predicate of state vectors, and
⊗f is a function from state vectors to state vectors.  Putting labels,
a conditional qgo and an assignment all into every statement is 
merely a convenience in giving the theory.  The more usual ways of
writing such programs are obtainable by specializing this general form.

	#. If ⊗u and ⊗v are programs, so is %2u_∪_v%1.  We can
take union rather than concatenation, because all statements have
labels.

Well-formedness

	Not every program is well-formed, because there may be
incompatible labels.  Therefore, we have a predicate ⊗ok(u) and two
auxiliary functions ⊗labels(u) and ⊗outlabels(u) satisfying
the following syntactic axioms in which free variables are assumed
universally quantified.

.item←0
#. %2ok elem(l1,p,f,l2,l3)

#. labels elem(l1,p,f,l2,l3) = α{l1α}

#. outlabels elem(l1,p,f,l2,l3) = α{l2,l3α}

#. ok (u ∪ v) ≡ ok u ∧ ok v ∧ labels(u) ∩ labels(v) = α{α}

#. labels(u ∪ v) = labels(u) ∪ labels(v)

#. outlabels(u ∪ v) = (outlabels(u) ∪ outlabels(v)) \ (labels(u) ∪ labels(v))%1

	A program ⊗u may be called complete if %2outlabels(u) =α{doneα}%1,
where ⊗done is a distinguished label denoting the end of the program.


Semantics

	The semantics of ⊗F1 is given by a predicate ⊗whither 
and a partial function ⊗outome.  %2whither(l1,u,l2,qx)%1 is true
if entering the
program ⊗u at label ⊗l1 in state qx will result in an exit at ⊗l2. 
%2outcome(l1,u,qx)%1 is the state that results when the program
⊗u is entered at label ⊗l1 while in state qx.  ⊗whither and  ⊗outcome are
easily given for elementary programs.  Namely

	%2whither(l1,elem(l1',p,f,l2',l3'),l2,qx) ≡
l1 = l1' ∧ (qif p(qx) qthen l2 = l2' qelse l2 = l3')%1

and

	%2outcome(l1,elem(l1',p,f,l2',l3'),qx) =
qif l1 = l1' qthen (qif p(qx) qthen f(qx) qelse qx)%1.

We consider %2outcome(l1,elem(l1',p,f,l2',l3'),qx)%1 undefined if
⊗l1 and ⊗l1' are not equal.

	Next we need to define %2whither(l1,u_∪_v,l2,qx)%1 and
%2outcome(l1,u_∪_v,qx)%1.  This is more difficult, because control
may go back and forth between the statements of ⊗u and the statements
of ⊗v an arbitrary number of times, so we have a complicated recursion.

.begin nofill

%2whither(l1,u ∪ v,l2,qx) ≡
∂(15)		[l1 ε labels(u) ∧
∂(20)			whither(l1,u,l2,qx) ∨
∂(25)				∃l.l ≠ l2 ∧ whither(l1,u,l,qx)
∂(30)					∧ whither(l,u ∪ v,l2,outcome(l1,u,qx))]]
∂(15)		∨ [l1 ε labels(v) ∧
∂(20)			whither(l1,v,l2,qx) ∨
∂(25)				∃l.l ≠ l2 ∧ whither(l1,v,l,qx)
∂(30)					∧ whither(l,u ∪ v,l2,outcome(l1,v,qx))]]%1.

.end

%1Notice that this is a recursive characterization of %2whither(l1,u_∪_v,l2,qx)%1, 
since the function being characterized appears on both sides of the formula.
%2outcome(l,u_∪_v,qx)%1 is determined by the relations

	%2l ε labels(u) ∧ whither(l,u,l2,qx) ∧ ¬(l2 ε labels(v)) ⊃
outcome(l,u_∪_v,qx) = outcome(l,u,qx)%1,

	%2l ε labels(v) ∧ whither(l,v,l2,qx) ∧ ¬(l2 ε labels(u)) ⊃
outcome(l,u_∪_v,qx) = outcome(l,v,qx)%1,

	%2l ε labels(u) ∧ whither(l,u,l2,qx) ∧ l2 ε labels(v) ⊃
outcome(l,u_∪_v,qx) = outcome(l2,u_∪_v,outcome(l,u,qx))%1

and

	%2l ε labels(v) ∧ whither(l,v,l2,qx) ∧ l2 ε labels(u) ⊃
outcome(l,u_∪_v,qx) = outcome(l2,u_∪_v,outcome(l,v,qx))%1.

	A theorem is required whose proof is likely to be tedious.
Namely, %2whither(l1,u,l2,qx)%1 and %2outcome(l,u,qx)%1 do not depend on
how the program ⊗u is built up from its elementary constituents.